COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 
C00011 00003	%7Corollary 13.1%1  Every recursive relation (or set) is expressible in ENT.
C00012 00004	
C00016 00005	.begin turn on "↑","]","["
C00019 00006	Thus, g is a one-one function from the set of symbols, expressions, and
C00031 ENDMK
C⊗;
 
A ⊗→number-theoretic function↔← is one whose arguments and values are natural
numbers, and a ⊗→number-theoretic relation↔← is a relation whose arguments are 
natural numbers.  For example, multiplication is a number-theoretic function
of two arguments, and the expression πx+πy<πz determines a number-theoretic
relation of three arguments.  Number-theoretic functions and relations are
intuitive and are not bound up with any formal system.

A number-theoretic relation πR(πx1n) is said to be %3⊗→expressible↔←%1 in ENT
iff there is a wff ?A(?x1n) of ENT with πn free variables such that for
any natural numbers πk1n
.begin nofill; indent 10,10;
1) if πR(πk1n) is true, then ?ε?A(λk1n)
2) if πR(πk1n) is false, then ?ε~?A(λk1n)
.fill;
where λk=λ0''%8...%1' (the kth successor of λ0), or simply the numeral
representing πk if we let the numerals λ1, λ2, λ3, ... represent respectively
the 1st, 2nd, 3rd, etc., successors of λ0.
.end
.begin indent 15,15;
For example: the number theoretic relation of equality is expressed
in ENT by the wff λx1=λx2.  In fact, if πk1=πk2 then λk1 is the same term
as λk2, and so by Lemma 2 a), {yon (R9)}, ?ελk1=λk2.  Also, if
πk1≠πk2, then ?ελk1≠λk2.

Likewise, the relation "less than" is expressed in ENT by the wff λx1<λx2.
For, if πk1<πk2, then there is some non-zero number πn such that
πk2=πk1+πn.  ?ελk2=λk1+λn, also since πn≠π0, ?ελn≠λ0.  So it is possible
to prove in ENT the wff (∃%dw%1)(λk2=λk1+%dw%1 ∧ %dw%1≠λ0), i.e., λk1<λk2.  
.end

It can also be shown that the negation, conjunction, and disjunction of
expressible relations are also expressible.

A number-theoretic function πf(πx1n) is said to be %3⊗→representable↔←%1 in ENT
iff there is a wff ?A(λx1n, λxn1) of ENT with the free variables λx1n, λxn1,
such that for any numbers πk1n, πk%4n+1%1
.begin nofill; indent 10,10;
1) if πf(πk1n)=πk%4n+1%1 then ?ε?A(λk1n, λk%4n+1%1)
2) ?ε(∃! λxn1)?A(λk1n, λxn1)
.end
If, in this definition, we change 2) to
.begin nofill; indent 10,10;
2') ?ε(∃! λxn1)?A(λx1n, λxn1)
.end
then the function πf is said to be %3⊗→strongly representable↔←%1 (in ENT)⊗↓The notation
"##!" is read "there exists a unique".←.  It
can be shown (see Mendelson [8]) that a function is representable iff
strongly representable.  Therefore we can use either 2) or 2') to determine
representability.

.R10:
.begin indent 10,13;
Examples: a) The zero function, πZ(πx)=π0, is representable by the wff
(λx1=λx1)∧(λx2=λ0).  For any πk1, if πZ(πk1)=πk2, then πk2=π0, and 
?ε(λk1=λk1)∧(λ0=λ0); thus 1) holds.  Also, ?ε(∃!#λx2)(λx1=λx1∧λx2=λ0); thus 2') holds.

b) The successor function, πN(πx)=πx+π1, is representable by the wff
λx2=λx1'.  For any πk1, if πN(πk1)=πk2, then πk2=πk1+π1, hence λk2=λk1'.
 Then ?ελk2=λk1'.  Also ?ε(∃! λx2)(λx2=λx1').

c) The projection function, πUni(πx1n)=πxi, is representable by the wff
(λx1=λx1)∧(λx2=λx2)∧...∧(λxn=λxn)∧(λxn1=λxi)

d) Assume that the functions πg(πx1, ..., πxm), πh1(πx1n), ..., πhm(πx1n)
are representable by the wffs ?B(λx1, ..., λx%4m+1%1),
?A%41%1(λx1, ..., λxn1), ..., ?A%4m%1(λx1, ..., λxn1),
respectively.  Define πf by the equation 
πf(πx1n)=πg(πh1(πx1n), ..., πhm(πx1n)), i.e., πf is obtained from πg, πh1, ..., πhm
by substitution.  Then πf is also representable, by the wff 
?A(λx1,#...,#λxn1)#:#(∃λy1)...(∃λym)(?A%41%1(λx1n, λy1)∧...∧?A%4m%1(λx1n, λym)∧?B(λy1, ..., λym, λxn1))
.end
.begin indent 10,10;
For proofs of the above, and the next three Lemmas, see Mendelson [8].
.end

.R5:
%7LEMMA 10%1   πR(πx1n) is expressible in ENT iff its characteristic function
πCR(πx1n) is representable in ENT.

%7LEMMA 11%1 (⊗→G%5o%1del's %gb%1-function↔←)   Let ⊗b(πx1, πx2, πx3) = %3rm%1(π1+(πx3+π1)⊗xπx2, πx1),
(remainder upon division of πx1 by π1+(πx3+π1)⊗xπx2).  Then ⊗b is primitive
recursive.  Also, ⊗b(πx1, πx2, πx3) is representable in ENT by the wff
.begin center;
λBt(λx1, λx2, λx3, λx4)#:#(∃λy)(λx1=(λ1+(λx3+λ1)⊗xλx2)⊗xλy+λx4 ∧ λx4<λ1+(λx3+λ1)⊗xλx2)
.end

%7LEMMA 12%1  For any sequence of natural numbers πk%40%1, πk1, πk2, ..., πkn,
there exist natural numbers %3b, c%1, such that ⊗b(%3b,#c,#i%1)#=#πki for π0≤πi≤πn.


%7THEOREM 13%1  Every recursive function is representable in ENT.
.begin nofill;
Sketch of proof:
.end
.begin indent 10,10;
The initial functions πZ, πN, πUni are representable in ENT, by examples 
a)-c) {yon (R10)}.  The Substitution Rule does not lead out of the class
of representable functions by example d).

The Recursion Rule:  assume that πg(πx1n) and πh(πx1n, πy, πz) are representable
by the wffs ?A(λx1, ..., λxn1) and ?B(λx1, ..., λxn3) respectively, and let
.begin center;
πf(πx1n, π0) = πg(πx1n)
πf(πx1n, πy+π1) = πh(πx1n, πy, πf(πx1n, πy)
.end
Now, πf(πx1n, πy) = πz iff there is a finite sequence of numbers πb0, ..., πby,
such that πb0=πg(πx1n), πb%4w+1%1=πh(πx1n, %3w%1, πb%4w%1) for πw+π1≤πy, and
πby=πz.  By Lemma 12 reference to finite sequences can be paraphrased in
terms of the function ⊗b, and by Lemma 11, ⊗b is representable.  In fact,
πf(πx1n, πxn1) is representable in ENT by the wff:
.begin nofill;
λC(λx1, ..., λxn2) :
   %1(∃λu)(∃λv)[((∃λw)(%dBt(u, v, 0, w) ∧ ?A(λx1n, %dw)))  ∧
       Bt(u, v, λxn1, λxn2%d)  ∧
            (∀w)(w<λxn1%d ⊃
		  %1(∃λy)(∃λz)(%dBt(u, v, w', y) ∧ Bt(u, v, w, z) ∧?B(λx1n, %dw, y, z))]%1
.end
.group
The ?m-operator:  assume that for any πx1n, there is some πy such that
πg(πx1n,#πy)#=#π0, and let us assume πg is representable by a wff 
?D(λx1, ..., λxn2).  Let πf(πx1n) = ?mπy(πg(πx1n, πy)=π0).  Then πf is 
representable by the wff 
.begin nofill;
	%dE%1(λx1, ..., λxn1): 
		?D(λx1, ..., λxn1, λ0) ∧ (∀λy)(λy<λxn1⊃~?D(λx1n, λy, λ0))
.apart
.end
.end
%7Corollary 13.1%1  Every recursive relation (or set) is expressible in ENT.
.begin nofill; indent 0,10;
Proof:
.fill;
Let πR(πx1n) be a recursive relation.  Then its characteristic function πCR is
recursive.  By Theorem 13, πCR is representable in ENT and therefore, by
Lemma 10, πR is expressible in ENT.
.end

We are now going to see that anything which can be expressed in ENT can be
mapped onto a unique positive integer.  This correlation of numbers with
symbols, expressions, and sequences of expressions was originally devised
by G⊗odel  in order to arithmetize metamathematics, i.e., to replace
assertions about a formal system by equivalent number-theoretic statements,
and then to express these statements within the formal system. 

 An %3
⊗→arithmetization↔←%1 of a first-order theory ⊗K is a one-one function ⊗g from
the set of symbols of ⊗K, expressions of ⊗K, and finite sequences of 
expressions of ⊗K, into the set of positive integers, such that the 
following conditions are satisfied:
.begin nofill; indent 10,10;
1)  ⊗g is effectively computable; and
.fill;
2)  there is an effective procedure which determines whether any given
positive integer πm is in the range of ⊗g, and if πm is in the range of
⊗g, the procedure finds the object ?x such that ⊗g(?x)=πm.
.end

This idea turned out to be the key to a great number of significant 
problems in mathematical logic.  We will see this kind of mapping again
when we look at LISP and map the theory into the domain of symbolic
expressions.

We correlate with each symbol ?u of a first order theory, ⊗K,
 a positive integer ⊗g(?u), called
the ⊗→G%5o%1del number↔← of ?u, in the following way:
.begin nofill; indent 15,15;
⊗g(%d(%1)=π3;  ⊗g(%d)%1)=π5;  ⊗g(%d,%1)=π7;  
⊗g(%d~%1)=π9;  ⊗g(%d⊃%1)=π11;  ⊗g(%d∀%1)=π13
⊗g(λxk)=π7+π8πk  for πk=π1, π2, ...
⊗g(λa%4k%1)=π9+π8πk  for πk=π1, π2, ...
⊗g(%df%8n%4k%1)=π11+π8(π2%8n%33%8k%1) for πk, πn ≥ π1###⊗↓We 
shall now be writing function and predicate letters 
with superscripts to denote the number of arguments 
they take.←
⊗g(%dA%8n%4k%1)=π13+π8(π2%8n%33%8k%1) for πk, πn ≥ π1
.end
Thus different symbols have different G⊗odel numbers, and every G⊗odel number
of a symbol is an odd positive integer.  For ENT we only have one constant, one
predicate, and three function symbols, rather than a denumerable number of each.  This
numbering is applicable to %2any%1 first order theory with the given symbols.
.begin turn on "↑","]","[";
Given an expression (i.e. sequence of symbols) ?u1?u2#...#?ur, we define its G⊗odel number
to be ⊗g(?u1?u2#...#?ur)#=#π2↑[⊗g(?u1)]⊗xπ3↑[⊗g(?u2)]⊗x#...#⊗xπpr↑[⊗g(?ur)],
where πpi is the i%8th%1 prime.

For example, ⊗g(λA%82%41%1(λx1, λx2)) = 
π2↑[⊗g(λA%82%41%1)]⊗xπ3↑[⊗g( ( )]⊗x#π5↑[⊗g(λx1)]⊗xπ7↑[⊗g( , )]⊗x#π11↑[⊗g(λx2)]⊗xπ13↑[⊗g( ) )];
or %32↑[109]⊗x%33↑3⊗x%35↑[15]⊗x%37↑7⊗x%311↑[23]⊗x%313↑5 .⊗↓%1Note that we have carefully designated
superscripts in the correct font; in the future we will use a more compact
representation: 
%32%8109%1⊗x3%83%1⊗x5%815%1⊗x7%87%1⊗x11%823%1⊗x13%85%1  to condense the printed 
form and aid in typing. The reader should have no difficulty in decoding the
abbreviations.←.
.end

By the unique factorization of the integers into primes we know that 
different expressions have different G⊗odel numbers.
In addition, expressions and symbols have different G⊗odel numbers since 
the former have even G⊗odel numbers, and the latter have odd numbers⊗↓A single
symbol considered as an expression has a different number from its number as a symbol.←.

If we have an arbitrary finite sequence of expressions, ?e1,#?e2,#...,#?er,
we can assign a G⊗odel number to this sequence by setting
.begin center
⊗g(?e1?e2#...#?er) = π2%8g(e1)%1⊗xπ3%8g(e2)%1⊗x#...#⊗xπpr%8g(er)%1.
.end
Different sequences of expressions will have different G⊗odel numbers.
Since a G⊗odel number of a sequence of expressions is even and the exponent of π2
in its prime factorization is also even, it differs from G⊗odel numbers of
symbols and expressions.
Thus, ⊗g is a one-one function from the set of symbols, expressions, and
finite sequences of expressions of ENT, into the set of positive integers.  The
range of ⊗g is not the entire set of positive integers; for example, %314%1 is
not a G⊗odel number.  The assignment of G⊗odel numbers given here is in no
way unique.  It has been taken with minor changes from Mendelson, another
method is used by Kleene, and there are more.

To facilitate definitions (and avoid trying to think up too many consecutive
primes) we define a ⊗→juxtaposition function *↔←:
.begin indent 10,10;
If ?x=π2%8a0%33%8a1%1⊗x⊗x⊗x%3p%8ak%4k%1 "represents" the sequence of positive
integers πa0, πa1, ..., πak, and ?y=π2%8b0%33%8b1⊗x⊗x⊗x%3p%8bm%4m%1 
"represents" the sequence πb0, πb1, ..., πbm, then the number
?x*?y=π2%8a0%33%8a1⊗x⊗x⊗x%3p%8ak%4k%3p%8b0%4k+1%3p%8b1%4k+2⊗x⊗x⊗x%3p%8bm%4k+1+m%1
"represents" the new sequence πa0,#πa1,#...,#πak,#πb0,#πb1,#...,#πbm obtained
by juxtaposing the two original sequences.  ( For a proof that * is both
primitive recursive and associative see Mendelson [8])

.end
.R2:
Also, we define the selector function ⊗→( )%4i%1↔← as follows:  with ?y as above,
(?y)%4i%1=πbi.

%7THEOREM 14%1###For ENT, the following relations and functions (1-7) are
recursive.
.begin "foo" indent 10,10;
1) %3EVbl(x)%1: πx is the number of an expression consisting of a variable.
(∃πz)%4z<x%1(π1≤πz#∧#πx#=#π2%87+8z%1). By theorem 8 this relation is
primitive recursive. Note that our numbering system 
allows us to put a bound on our search for πz, since the number of any expression
must be larger than that of any part (exponent, addend, multiplier) of it.

2) %3MP(x, y, z)%1: the expression with G⊗odel number πz
is a direct consequence of the expressions with G⊗odel numbers πx and πy by Modus
Ponens. πy#=#π2%83%1*πx*π2%811%1*πz*π2%85%1. 
Running back and forth to see which symbols are represented by which numbers, we can
decode the above to find πy represents "λx#⊃#λz", where ⊗g(λx)=πx and ⊗g(λz)=πz.

However matters get worse from here and it is easy to get lost in the numbers.
Hopefully  having been convinced of the correctness of the numbering,
we can dispose of the concrete syntax  in favor of an abstract syntax which
is more readable than strings of exponents. For example:
.begin nofill;select 3;
MP(x, y, z) <= [is_impl(y) → is_ant(x,y) → is_cons(z,y)
				T   →   false
			T  →  false]
.end
.begin nofill;        
where: %3is_impl(y)%1 means "is πy (the G⊗odel number of) an implication"
			i.e. (∃πx1)%4x1<y%1(∃πx2)%4x2<y%1 πy=π2%83%1*πx1*π2%811%1*πx2*π2%85%1
	%3is_ant(x,y)%1 means "is πx the antecedent of πy"
	%3is_cons(z,y)%1 means "is πz the consequent of πy"
	%3T%1 is simply an "otherwise" condition
This style of definition is recursive by Theorem 9.

.begin tabit1 (25);
3) %3is_Fml(y): y%1 is the G⊗odel number of a wff
%3is_Fml(y) <= \[is_Atfml(y)
\is_Imp(y) → is_Fml(Ant(y)) → is_Fml(Cons(y))
\is_Neg(y) → is_Fml(Body(y))
\is_Forall(y) → is_Fml(Body(y))
\T   →   false]%1
.end
.end
If πy is a wff it must be an atomic formula, an implication, a negation, or a
generalization of some formula, otherwise πy is not a wff.  The selectors
%3"Ant"%1 and %3"Cons"%1 pick out the antecedent and consequent parts of an
implication, %3Body(y)%1 will strip a negation or generalization off of πy
leaving the part negated or generalized.  Using the concrete syntax, the
first clause of the definition would take up more space than the entire
description above.  However every clause is not so bad as %3is_Atfml(y)%1,
for %3is_Neg(y) → is_Fml(Body(y))%1 we could have written:
.begin center;
(∃πz)%4z<y%1[%3is_Fml(z) ∧ y=2%83%1*π2%89%1*πz*π2%85%1]
.end
Even this is not completely concrete as we have used %3is_Fml%1 instead of
its encoding in numbers.  And so we bid farewell to concrete syntax.  We
will instead describe abstractly what recognizers and selectors we may need
and how they work.

.begin indent 10,15;
4) a) %3Pf(y, x)%1 is a recognizer; it will utilize another recognizer which
tells us whether or not πy is the G⊗odel number of a sequence of wffs
obeying the formation rules for a proof, and a selector which picks off the
last wff of the sequence which can then be compared with the wff with
G⊗odel number πx to see if we have a proof of the formula we want.
.end
.begin indent 12,15;
b) Let ?A(?x1n) be a fixed wff of ENT containing ?x1n as its only free
variables, and let πm be the G⊗odel number of ?A(?x1n).  Let
πBWa(πu1, ..., πun, πy) mean: πy is the G⊗odel number of a proof of
?A(λu1, λu2, ..., λun).
.end

5) %3Sub(y, u, v)%1 is the G⊗odel number of the result of substituting the 
term with G⊗odel number πu for all free occurrences of the variable with
G⊗odel number πv in the expression with G⊗odel number πy.

.W1:
.begin indent 10,15;
6) a) ⊗→%3W%41%1(%3u%1, %3y%1)↔←: πu is the G⊗odel number of a wff ?A(λx1) containing
the free variable λx1, and πy is the G⊗odel number of a proof of ?A(λu).
This is equivalent to:
.begin nofill;
	%3is_Fml(u) ∧ is_FreeVar(u, 2%815%3) ∧ πBWa%3(u, y)
%1				or,
	%3is_Fml(u) → is_FreeVar(u,2%815%3) → Pf(y, Sub(u, Num(u), 2%815%3)
				T    →    false
		T   →  false
.end
%3Num(u)%1 is the g⊗odel number of the term (numeral) λu.
Note that substituting λu into ?A for λx1 makes ?A(λu) a formula which states
something about itself.
.end

.begin indent 15,15;
b) πW2(πu, πy): πu is the G⊗odel number of a wff ?A(λx1) containing the free
variable λx1, and πy is the G⊗odel number of a proof of ~?A(λu).  Then
πW2(πu, πy) is a true statement if πy is the G⊗odel number of a proof that
the statement ?A applied to itself is false.
.end

.R11:
7)  We define a function ⊗→%3D%1(%3u%1)↔← such that, if πu is the G⊗odel number of a wff
?A(λx1) with the free variable λx1, then πD(πu) is the G⊗odel number of
?A(λu).  So πD(πu) = %3Sub(u, Num(u), π2%815%3)%1

.end "foo"
For proofs that the functions given above are in fact recursive see Mendelson [8].

%7THEOREM 15%1###Any function πf(πx1n) which is representable in ENT is recursive.
.begin nofill;
Proof:
.end
.begin indent 10,10;
Let ?A(λx1n, λz) be a wff representing πf.  Consider the natural numbers
πk1,#...,#πkn.  Let πf(πk1,#...,#πkn)#=#πm.  Then ?ε?A(λk1,#...,#λkn,#λm).  Let
πj be the G⊗odel number of a proof in ENT of ?A(λk1,#...,#λkn,#λm).
Then πBWa(πk1n,#πm,#πj).  So, for any πx1n there is some πy such that
πBWa(πx1n, (πy)%40%1, (πy)%41%1). ⊗↓The selectors ( )%4i%1 were defined on {yon (R2)}←

Then πf(πx1n) = (?mπy(πBWa(πx1n, (πy)%40%1, (πy)%41%1)))%40%1.  πBWa is recursive,
hence, by the ?m-operator Rule (VI), ?mπy(πBWa(πx1n,#(πy)%40%1,#(πy)%41%1)) is
recursive, and therefore, so is πf.

.end
Thus, by Theorems 13 and 15, we have that a number-theoretic function is recursive
iff it is representable in ENT.

.group
%7Corollary 15.1 %1###A number-theoretic relation πR(πx1n) is recursive iff
πR(πx1n) is expressible in ENT.  (In particular, a set is recursive iff expressible.)
.apart